Nuprl Lemma : eq_id_test
0,22
postcript
pdf
("x" = "x" ~ true
) & ("x" = "y" ~ false
)
latex
Definitions
P
&
Q
,
eq_atom$n(
x
;
y
)
,
Atom2Deq
,
eqof(
d
)
,
IdDeq
,
a
=
b
,
"$x"
origin
) & ("x" = "y" ~ false) ) & ("x" = "y" ~ false)